$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $j$:E. ($\forall$$e$:E. ($e$ $<$ $j$) $\Rightarrow$ Dec($P$($e$))) $\Rightarrow$ Dec($\exists$$k$:E. (($k$ $<$ $j$) \& $P$($k$)))